Nuprl Lemma : csinput?_wf
11,40
postcript
pdf
Cmd
:Type,
x
:chain_sys(
Cmd
). csinput?(
x
)
latex
Definitions
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
csinput?(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s1
,
s2
)
,
x
(
s
)
Lemmas
chain
sys
wf
,
Id
wf
,
bfalse
wf
,
btrue
wf
,
bool
wf
,
chain
sys
ind
wf
origin
Cmd:Type, x:chain_sys(Cmd). csinput?(x) 
Cmd:Type, x:chain_sys(Cmd). csinput?(x) 
x,y. t(x;y)x. t(x) Tx:A. B(x)